YES 3.193 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ LR

mainModule List
  ((elemIndices :: (Eq b, Eq a) => Either a b  ->  [Either a b ->  [Int]) :: (Eq b, Eq a) => Either a b  ->  [Either a b ->  [Int])

module List where
  import qualified Maybe
import qualified Prelude

  elemIndices :: Eq a => a  ->  [a ->  [Int]
elemIndices x findIndices (== x)

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (\vv1 ->
case vv1 of
  (x,i)->  if p x then i : [] else []
  _-> []
) (zip xs (enumFrom 0))


module Maybe where
  import qualified List
import qualified Prelude



Lambda Reductions:
The following Lambda expression
\vv1
case vv1 of
 (x,i) → if p x then i : [] else []
 _ → []

is transformed to
findIndices0 p vv1 = 
case vv1 of
 (x,i) → if p x then i : [] else []
 _ → []

The following Lambda expression
\ab→(a,b)

is transformed to
zip0 a b = (a,b)



↳ HASKELL
  ↳ LR
HASKELL
      ↳ CR

mainModule List
  ((elemIndices :: (Eq b, Eq a) => Either a b  ->  [Either a b ->  [Int]) :: (Eq a, Eq b) => Either a b  ->  [Either a b ->  [Int])

module List where
  import qualified Maybe
import qualified Prelude

  elemIndices :: Eq a => a  ->  [a ->  [Int]
elemIndices x findIndices (== x)

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 
case vv1 of
  (x,i)->  if p x then i : [] else []
  _-> []


module Maybe where
  import qualified List
import qualified Prelude



Case Reductions:
The following Case expression
case vv1 of
 (x,i) → if p x then i : [] else []
 _ → []

is transformed to
findIndices00 p (x,i) = if p x then i : [] else []
findIndices00 p _ = []



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
HASKELL
          ↳ IFR

mainModule List
  ((elemIndices :: (Eq b, Eq a) => Either b a  ->  [Either b a ->  [Int]) :: (Eq a, Eq b) => Either b a  ->  [Either b a ->  [Int])

module List where
  import qualified Maybe
import qualified Prelude

  elemIndices :: Eq a => a  ->  [a ->  [Int]
elemIndices x findIndices (== x)

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 findIndices00 p vv1

  
findIndices00 p (x,i if p x then i : [] else []
findIndices00 p _ []


module Maybe where
  import qualified List
import qualified Prelude



If Reductions:
The following If expression
if p x then i : [] else []

is transformed to
findIndices000 i True = i : []
findIndices000 i False = []



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
HASKELL
              ↳ BR

mainModule List
  ((elemIndices :: (Eq b, Eq a) => Either a b  ->  [Either a b ->  [Int]) :: (Eq a, Eq b) => Either a b  ->  [Either a b ->  [Int])

module List where
  import qualified Maybe
import qualified Prelude

  elemIndices :: Eq a => a  ->  [a ->  [Int]
elemIndices x findIndices (== x)

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 findIndices00 p vv1

  
findIndices00 p (x,ifindIndices000 i (p x)
findIndices00 p _ []

  
findIndices000 i True i : []
findIndices000 i False []


module Maybe where
  import qualified List
import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
HASKELL
                  ↳ COR

mainModule List
  ((elemIndices :: (Eq a, Eq b) => Either a b  ->  [Either a b ->  [Int]) :: (Eq a, Eq b) => Either a b  ->  [Either a b ->  [Int])

module List where
  import qualified Maybe
import qualified Prelude

  elemIndices :: Eq a => a  ->  [a ->  [Int]
elemIndices x findIndices (== x)

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 findIndices00 p vv1

  
findIndices00 p (x,ifindIndices000 i (p x)
findIndices00 p vw []

  
findIndices000 i True i : []
findIndices000 i False []


module Maybe where
  import qualified List
import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
HASKELL
                      ↳ NumRed

mainModule List
  ((elemIndices :: (Eq a, Eq b) => Either b a  ->  [Either b a ->  [Int]) :: (Eq a, Eq b) => Either b a  ->  [Either b a ->  [Int])

module List where
  import qualified Maybe
import qualified Prelude

  elemIndices :: Eq a => a  ->  [a ->  [Int]
elemIndices x findIndices (== x)

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 findIndices00 p vv1

  
findIndices00 p (x,ifindIndices000 i (p x)
findIndices00 p vw []

  
findIndices000 i True i : []
findIndices000 i False []


module Maybe where
  import qualified List
import qualified Prelude



Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
HASKELL
                          ↳ Narrow

mainModule List
  (elemIndices :: (Eq a, Eq b) => Either a b  ->  [Either a b ->  [Int])

module List where
  import qualified Maybe
import qualified Prelude

  elemIndices :: Eq a => a  ->  [a ->  [Int]
elemIndices x findIndices (== x)

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (findIndices0 p) (zip xs (enumFrom (Pos Zero)))

  
findIndices0 p vv1 findIndices00 p vv1

  
findIndices00 p (x,ifindIndices000 i (p x)
findIndices00 p vw []

  
findIndices000 i True i : []
findIndices000 i False []


module Maybe where
  import qualified List
import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(yu7100), Succ(yu411000000)) → new_primPlusNat(yu7100, yu411000000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(yu30000), Succ(yu41100000)) → new_primMulNat(yu30000, Succ(yu41100000))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(yu3000), Succ(yu4110000)) → new_primEqNat(yu3000, yu4110000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs1(Left(@2(yu300, yu301)), Left(@2(yu411000, yu411001)), app(app(ty_@2, app(ty_Maybe, bbh)), bbb), gc) → new_esEs2(yu300, yu411000, bbh)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), cc, cd, app(app(ty_Either, db), dc)) → new_esEs1(yu302, yu411002, db, dc)
new_esEs1(Left(:(yu300, yu301)), Left(:(yu411000, yu411001)), app(ty_[], app(ty_[], bb)), gc) → new_esEs(yu300, yu411000, bb)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), app(ty_Maybe, fh), cd, dh) → new_esEs2(yu300, yu411000, fh)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), cc, cd, app(ty_Maybe, dd)) → new_esEs2(yu302, yu411002, dd)
new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, app(app(ty_@2, ga), gb)), cd), dh), gc) → new_esEs3(yu300, yu411000, ga, gb)
new_esEs1(Right(yu30), Right(yu41100), bcc, app(app(app(ty_@3, bce), bcf), bcg)) → new_esEs0(yu30, yu41100, bce, bcf, bcg)
new_esEs1(Left(Just(yu300)), Left(Just(yu411000)), app(ty_Maybe, app(app(ty_@2, he), hf)), gc) → new_esEs3(yu300, yu411000, he, hf)
new_esEs3(@2(yu300, yu301), @2(yu411000, yu411001), app(ty_[], bba), bbb) → new_esEs(yu300, yu411000, bba)
new_esEs3(@2(yu300, yu301), @2(yu411000, yu411001), app(app(app(ty_@3, bbc), bbd), bbe), bbb) → new_esEs0(yu300, yu411000, bbc, bbd, bbe)
new_esEs1(Left(yu30), Left(yu41100), app(app(ty_Either, gd), ge), gc) → new_esEs1(yu30, yu41100, gd, ge)
new_esEs2(Just(yu300), Just(yu411000), app(ty_Maybe, hd)) → new_esEs2(yu300, yu411000, hd)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), cc, cd, app(ty_[], ce)) → new_esEs(yu302, yu411002, ce)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), cc, app(app(ty_Either, ed), ee), dh) → new_esEs1(yu301, yu411001, ed, ee)
new_esEs1(Left(@2(yu300, yu301)), Left(@2(yu411000, yu411001)), app(app(ty_@2, hg), app(app(app(ty_@3, baa), bab), bac)), gc) → new_esEs0(yu301, yu411001, baa, bab, bac)
new_esEs3(@2(yu300, yu301), @2(yu411000, yu411001), hg, app(ty_[], hh)) → new_esEs(yu301, yu411001, hh)
new_esEs1(Left(Just(yu300)), Left(Just(yu411000)), app(ty_Maybe, app(app(app(ty_@3, gg), gh), ha)), gc) → new_esEs0(yu300, yu411000, gg, gh, ha)
new_esEs1(Left(@2(yu300, yu301)), Left(@2(yu411000, yu411001)), app(app(ty_@2, hg), app(ty_[], hh)), gc) → new_esEs(yu301, yu411001, hh)
new_esEs2(Just(yu300), Just(yu411000), app(app(app(ty_@3, gg), gh), ha)) → new_esEs0(yu300, yu411000, gg, gh, ha)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), app(app(ty_@2, ga), gb), cd, dh) → new_esEs3(yu300, yu411000, ga, gb)
new_esEs1(Left(@2(yu300, yu301)), Left(@2(yu411000, yu411001)), app(app(ty_@2, app(app(app(ty_@3, bbc), bbd), bbe)), bbb), gc) → new_esEs0(yu300, yu411000, bbc, bbd, bbe)
new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, app(app(ty_Either, ff), fg)), cd), dh), gc) → new_esEs1(yu300, yu411000, ff, fg)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), cc, app(ty_[], dg), dh) → new_esEs(yu301, yu411001, dg)
new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, cc), cd), app(ty_Maybe, dd)), gc) → new_esEs2(yu302, yu411002, dd)
new_esEs3(@2(yu300, yu301), @2(yu411000, yu411001), app(app(ty_@2, bca), bcb), bbb) → new_esEs3(yu300, yu411000, bca, bcb)
new_esEs1(Left(@2(yu300, yu301)), Left(@2(yu411000, yu411001)), app(app(ty_@2, app(app(ty_@2, bca), bcb)), bbb), gc) → new_esEs3(yu300, yu411000, bca, bcb)
new_esEs1(Left(:(yu300, yu301)), Left(:(yu411000, yu411001)), app(ty_[], app(app(ty_@2, ca), cb)), gc) → new_esEs3(yu300, yu411000, ca, cb)
new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, cc), app(app(ty_@2, eg), eh)), dh), gc) → new_esEs3(yu301, yu411001, eg, eh)
new_esEs3(@2(yu300, yu301), @2(yu411000, yu411001), hg, app(app(app(ty_@3, baa), bab), bac)) → new_esEs0(yu301, yu411001, baa, bab, bac)
new_esEs1(Right(yu30), Right(yu41100), bcc, app(ty_[], bcd)) → new_esEs(yu30, yu41100, bcd)
new_esEs1(Left(Just(yu300)), Left(Just(yu411000)), app(ty_Maybe, app(ty_[], gf)), gc) → new_esEs(yu300, yu411000, gf)
new_esEs1(Left(Just(yu300)), Left(Just(yu411000)), app(ty_Maybe, app(ty_Maybe, hd)), gc) → new_esEs2(yu300, yu411000, hd)
new_esEs1(Right(yu30), Right(yu41100), bcc, app(ty_Maybe, bdb)) → new_esEs2(yu30, yu41100, bdb)
new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, cc), cd), app(app(ty_Either, db), dc)), gc) → new_esEs1(yu302, yu411002, db, dc)
new_esEs1(Left(@2(yu300, yu301)), Left(@2(yu411000, yu411001)), app(app(ty_@2, hg), app(app(ty_@2, bag), bah)), gc) → new_esEs3(yu301, yu411001, bag, bah)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), cc, cd, app(app(ty_@2, de), df)) → new_esEs3(yu302, yu411002, de, df)
new_esEs2(Just(yu300), Just(yu411000), app(ty_[], gf)) → new_esEs(yu300, yu411000, gf)
new_esEs3(@2(yu300, yu301), @2(yu411000, yu411001), app(app(ty_Either, bbf), bbg), bbb) → new_esEs1(yu300, yu411000, bbf, bbg)
new_esEs3(@2(yu300, yu301), @2(yu411000, yu411001), hg, app(ty_Maybe, baf)) → new_esEs2(yu301, yu411001, baf)
new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, app(ty_[], fa)), cd), dh), gc) → new_esEs(yu300, yu411000, fa)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), app(app(ty_Either, ff), fg), cd, dh) → new_esEs1(yu300, yu411000, ff, fg)
new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, app(app(app(ty_@3, fb), fc), fd)), cd), dh), gc) → new_esEs0(yu300, yu411000, fb, fc, fd)
new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, cc), cd), app(app(ty_@2, de), df)), gc) → new_esEs3(yu302, yu411002, de, df)
new_esEs1(Left(:(yu300, yu301)), Left(:(yu411000, yu411001)), app(ty_[], ba), gc) → new_esEs(yu301, yu411001, ba)
new_esEs1(Left(@2(yu300, yu301)), Left(@2(yu411000, yu411001)), app(app(ty_@2, hg), app(app(ty_Either, bad), bae)), gc) → new_esEs1(yu301, yu411001, bad, bae)
new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, cc), app(app(ty_Either, ed), ee)), dh), gc) → new_esEs1(yu301, yu411001, ed, ee)
new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, cc), app(ty_[], dg)), dh), gc) → new_esEs(yu301, yu411001, dg)
new_esEs1(Right(yu30), Right(yu41100), bcc, app(app(ty_Either, bch), bda)) → new_esEs1(yu30, yu41100, bch, bda)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), cc, app(app(app(ty_@3, ea), eb), ec), dh) → new_esEs0(yu301, yu411001, ea, eb, ec)
new_esEs1(Left(@2(yu300, yu301)), Left(@2(yu411000, yu411001)), app(app(ty_@2, app(ty_[], bba)), bbb), gc) → new_esEs(yu300, yu411000, bba)
new_esEs(:(yu300, yu301), :(yu411000, yu411001), app(ty_Maybe, bh)) → new_esEs2(yu300, yu411000, bh)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), cc, app(app(ty_@2, eg), eh), dh) → new_esEs3(yu301, yu411001, eg, eh)
new_esEs1(Left(:(yu300, yu301)), Left(:(yu411000, yu411001)), app(ty_[], app(app(app(ty_@3, bc), bd), be)), gc) → new_esEs0(yu300, yu411000, bc, bd, be)
new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, cc), app(app(app(ty_@3, ea), eb), ec)), dh), gc) → new_esEs0(yu301, yu411001, ea, eb, ec)
new_esEs3(@2(yu300, yu301), @2(yu411000, yu411001), hg, app(app(ty_@2, bag), bah)) → new_esEs3(yu301, yu411001, bag, bah)
new_esEs2(Just(yu300), Just(yu411000), app(app(ty_Either, hb), hc)) → new_esEs1(yu300, yu411000, hb, hc)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), app(ty_[], fa), cd, dh) → new_esEs(yu300, yu411000, fa)
new_esEs(:(yu300, yu301), :(yu411000, yu411001), ba) → new_esEs(yu301, yu411001, ba)
new_esEs3(@2(yu300, yu301), @2(yu411000, yu411001), app(ty_Maybe, bbh), bbb) → new_esEs2(yu300, yu411000, bbh)
new_esEs3(@2(yu300, yu301), @2(yu411000, yu411001), hg, app(app(ty_Either, bad), bae)) → new_esEs1(yu301, yu411001, bad, bae)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), cc, cd, app(app(app(ty_@3, cf), cg), da)) → new_esEs0(yu302, yu411002, cf, cg, da)
new_esEs1(Left(@2(yu300, yu301)), Left(@2(yu411000, yu411001)), app(app(ty_@2, app(app(ty_Either, bbf), bbg)), bbb), gc) → new_esEs1(yu300, yu411000, bbf, bbg)
new_esEs1(Left(Just(yu300)), Left(Just(yu411000)), app(ty_Maybe, app(app(ty_Either, hb), hc)), gc) → new_esEs1(yu300, yu411000, hb, hc)
new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, cc), cd), app(app(app(ty_@3, cf), cg), da)), gc) → new_esEs0(yu302, yu411002, cf, cg, da)
new_esEs1(Left(:(yu300, yu301)), Left(:(yu411000, yu411001)), app(ty_[], app(ty_Maybe, bh)), gc) → new_esEs2(yu300, yu411000, bh)
new_esEs1(Left(@2(yu300, yu301)), Left(@2(yu411000, yu411001)), app(app(ty_@2, hg), app(ty_Maybe, baf)), gc) → new_esEs2(yu301, yu411001, baf)
new_esEs(:(yu300, yu301), :(yu411000, yu411001), app(app(app(ty_@3, bc), bd), be)) → new_esEs0(yu300, yu411000, bc, bd, be)
new_esEs1(Left(:(yu300, yu301)), Left(:(yu411000, yu411001)), app(ty_[], app(app(ty_Either, bf), bg)), gc) → new_esEs1(yu300, yu411000, bf, bg)
new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, app(ty_Maybe, fh)), cd), dh), gc) → new_esEs2(yu300, yu411000, fh)
new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, cc), cd), app(ty_[], ce)), gc) → new_esEs(yu302, yu411002, ce)
new_esEs(:(yu300, yu301), :(yu411000, yu411001), app(app(ty_@2, ca), cb)) → new_esEs3(yu300, yu411000, ca, cb)
new_esEs2(Just(yu300), Just(yu411000), app(app(ty_@2, he), hf)) → new_esEs3(yu300, yu411000, he, hf)
new_esEs(:(yu300, yu301), :(yu411000, yu411001), app(app(ty_Either, bf), bg)) → new_esEs1(yu300, yu411000, bf, bg)
new_esEs1(Right(yu30), Right(yu41100), bcc, app(app(ty_@2, bdc), bdd)) → new_esEs3(yu30, yu41100, bdc, bdd)
new_esEs1(Left(@3(yu300, yu301, yu302)), Left(@3(yu411000, yu411001, yu411002)), app(app(app(ty_@3, cc), app(ty_Maybe, ef)), dh), gc) → new_esEs2(yu301, yu411001, ef)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), cc, app(ty_Maybe, ef), dh) → new_esEs2(yu301, yu411001, ef)
new_esEs(:(yu300, yu301), :(yu411000, yu411001), app(ty_[], bb)) → new_esEs(yu300, yu411000, bb)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), app(app(app(ty_@3, fb), fc), fd), cd, dh) → new_esEs0(yu300, yu411000, fb, fc, fd)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_foldr(yu3, :(yu4110, yu4111), yu64, ba, bb) → new_foldr(yu3, yu4111, new_primPlusNat0(yu64, Zero), ba, bb)

The TRS R consists of the following rules:

new_primPlusNat0(Zero, yu41100000) → Succ(yu41100000)
new_primPlusNat0(Succ(yu710), yu41100000) → Succ(Succ(new_primPlusNat1(yu710, yu41100000)))
new_primPlusNat1(Succ(yu7100), Zero) → Succ(yu7100)
new_primPlusNat1(Zero, Succ(yu411000000)) → Succ(yu411000000)
new_primPlusNat1(Succ(yu7100), Succ(yu411000000)) → Succ(Succ(new_primPlusNat1(yu7100, yu411000000)))
new_primPlusNat1(Zero, Zero) → Zero

The set Q consists of the following terms:

new_primPlusNat1(Succ(x0), Zero)
new_primPlusNat0(Zero, x0)
new_primPlusNat1(Zero, Succ(x0))
new_primPlusNat1(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, Zero)
new_primPlusNat0(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: